$\forall$${\it es}$:ES, $A$:Type, $X$:AbsInterface($A$ List), $e$:E.
\\[0ex]($\uparrow$first($e$)) $\Rightarrow$ (es{-}interface{-}history(${\it es}$;$X$;$e$) = if $e$ $\in_{b}$ $X$ then $X$($e$) else [] fi  $\in$ ($A$ List))